Inference at * 1 1 1 1 
Iof proof for Lemma decidable implies better:

.....assertion..... NILNIL

1. P : 
2. Q : x:P.
3. P
4. Dec(Q)
  Q   

latex

 by RenameVar `x' (-2) THEN IsectHD x 2 THEN Auto 

latex

 .

Definitions

t  T